﻿using System;
using System.Collections.Generic;
using System.Text;
using System.Linq;

using System.Diagnostics.Contracts;

using SimpleIR;
using RgnAnalyzer.Domain;

namespace RgnAnalyzer
{
	/// <summary>
	/// This class contains a bunch of static/global accessors for states of the analysis that get used over wide parts of the analysis.
	/// Also serves as the launch point for various analysis phases and queries from external code.
	/// </summary>
	public static class GlobalAnalysisState
	{
		public static string GlobalDataDir;
		public static string SerializeDataDir;

		internal static MethodContextState MainMethodContext;

		//The program we are analyzing
		private static IRProgram s_prog;

		//The global state of the analysis of this program
		private static GlobalCallStateMap s_analysis;

		internal static PInfoModel.CompleteAnalysisInfoForProgram CompleteAnalysisResults;

		public static int MaxLoopFixIters = 0;
		
		private static void ResetRuntimeCtrs()
		{
			MaxLoopFixIters = 0;
		}

		public static void LoadProg(IRProgram p, string globaldatadir, string serializedir)
		{
			GlobalDataDir = globaldatadir;
			SerializeDataDir = serializedir;

			s_prog = p;
			s_analysis = new GlobalCallStateMap();
			s_analysis.InitializeForAnalysis(p.CallGraph, p.MethodBodyTable);
			ResetRuntimeCtrs();
		}

		public static void AnalyzeMain(bool intesting)
		{
			CompleteAnalysisResults = null;
			EscapeSiteInfo.EscapeIdentityCounter = -1;

			IRStaticInvoke maininv = s_prog.InvokeTable.GetMainInvoke();
			IRInvokeIdentity mainID = s_prog.InvokeTable.LookupInvokeIdentity(maininv.DefClass, maininv);
			IRBodyDef mainBody = s_prog.MethodBodyTable.GetBodyForInvokeExactSigMatch(mainID);
			
			//initialize the program model for the first run
			ALocation.ResetIDTagCtrForAnalysis();
			AProgramMemory initpm = new AProgramMemory();
			List<IRStaticField> sfv = new List<IRStaticField>();
			s_prog.NameTable.FillVectorWithAllStaticFields(sfv);
			initpm.IntialStateProgModel(sfv);
			
			//initialize the call to main and put it on the worklist
			MainMethodContext = s_analysis.HasMemoForCallAddMemoContextAsNeeded(mainBody, initpm, false, mainBody.InvokeID.DefInClass, new CallStateSubMap());
#if DEBUG
			MainMethodContext.DebugState = (intesting) ? DebugState.DebugRun : DebugState.DebugStepInto;
#endif
			s_analysis.EnqueueCalleeMethod(MainMethodContext, s_prog.CallGraph);

			RunAnalysisToCompletion();

			s_analysis.ClearUnUsedStates();
		}

		private static void RunAnalysisToCompletion()
		{
			bool done = s_analysis.ProcessNextPendingMethod(s_prog.CallGraph);
			while(!done)
			{
				Display__PrintPendingInfo();

				done = s_analysis.ProcessNextPendingMethod(s_prog.CallGraph);
			}
		}

		/// <summary>
		/// After analyzing the program fill in and convert the results to the full analysis info the program.
		/// </summary>
		public static PInfoModel.CompleteAnalysisInfoForProgram ComputeFullAnalysisInfo(bool computeprogpointinfo)
		{
			//
			Console.WriteLine("Starting Context Cleaning Pass");

			PInfoModel.CompleteAnalysisInfoMethodContext.CleanUpProgPointInfoTables();
			PInfoModel.CompleteAnalysisInfoMethodContext.InitializeProgPointInfoTables();

			DoSetupOfCompleteInfo(new Dictionary<IRInvokeIdentity, PInfoModel.CompleteAnalysisInfoMethod>(), new Dictionary<IRInvokeIdentity, Dictionary<int, int>>(), new Dictionary<IRInvokeIdentity, Dictionary<AExternalRef, AExternalRef>>(), false);
			CompleteAnalysisResults = null;

			//force clean contexts which are no longer needed
			HashSet<int> usefulcontexts = new HashSet<int>();
			s_analysis.ForceCleanUselessContexts(MainMethodContext, usefulcontexts);

			PInfoModel.CompleteAnalysisInfoMethodContext.CleanUpProgPointInfoTables();
			PInfoModel.CompleteAnalysisInfoMethodContext.InitializeProgPointInfoTables();
			System.GC.Collect();

			//
			Console.WriteLine("Starting Complete Info Pass");

			Dictionary<IRInvokeIdentity, PInfoModel.CompleteAnalysisInfoMethod> methodstates = new Dictionary<IRInvokeIdentity, PInfoModel.CompleteAnalysisInfoMethod>();
			Dictionary<IRInvokeIdentity, Dictionary<int, int>> methodidsimplify = new Dictionary<IRInvokeIdentity, Dictionary<int, int>>();
			Dictionary<IRInvokeIdentity, Dictionary<AExternalRef, AExternalRef>> methodextrsimplify = new Dictionary<IRInvokeIdentity, Dictionary<AExternalRef, AExternalRef>>();
			DoSetupOfCompleteInfo(methodstates, methodidsimplify, methodextrsimplify, computeprogpointinfo);

			List<Tuple<IRInvokeIdentity, List<MethodContextState>>> mcstl = s_analysis.GetAllMethodsAndContextsForInfoCompletion();
			PInfoModel.CompleteAnalysisInfoForProgram resv = CompleteAnalysisResults;
			CompleteAnalysisResults = null;

			//compute the summary information for each method invoke
			foreach(Tuple<IRInvokeIdentity, List<MethodContextState>> mcst in mcstl)
			{
				if(mcst.Item2.Count == 0)
					continue;

				AProgramMemory summaryin = null;
				AProgramMemory summaryout = null;

				PInfoModel.CompleteAnalysisInfoMethod cm = methodstates[mcst.Item1];

				foreach(MethodContextState mmcs in mcst.Item2)
				{
					//gather pre/post
					Tuple<AProgramMemory, AProgramMemory> resp = mmcs.GetInputOutputPairForCompleteInfo();
					PInfoModel.PIModel mout = (resp.Item2 != null) ? resp.Item2.MakePIModelForThis() : null;

					AProgramMemory cin = resp.Item1.CopyMemoryState();
					cin.NormalizeAtRecursiveCallEntry();
					summaryin = (summaryin != null) ? AProgramMemory.PMemoryMergeCallsEntry(summaryin, cin) : cin;

					if(mout != null)
					{
						AProgramMemory cout = resp.Item2.CopyMemoryState();
						cout.NormalizeAtRecursiveCallEntry();
						summaryout = (summaryout != null) ? AProgramMemory.PMemoryMergeCallsEntry(summaryout, cout) : cout;
					}

					//gather single context
					PInfoModel.CompleteAnalysisInfoMethodContext cmmc = cm.AllCallContexts.Find((PInfoModel.CompleteAnalysisInfoMethodContext ccf) => ccf.ContextID == mmcs.ContextID);
					cmmc.FinalizeInputAndOutputStates(mout);
				}

				Dictionary<int, int> idsimplifymap = methodidsimplify[mcst.Item1];
				Dictionary<AExternalRef, AExternalRef> extrsimplifymap = methodextrsimplify[mcst.Item1];

				Dictionary<PInfoModel.PIExternalRef, HashSet<PInfoModel.PIExternalRef>> erremap = new Dictionary<PInfoModel.PIExternalRef, HashSet<PInfoModel.PIExternalRef>>();
				Dictionary<int, HashSet<int>> idremap = new Dictionary<int, HashSet<int>>();
				AProgramMemory.FinalInfoComputeTidyInOutSummaries(summaryin, summaryout, idsimplifymap, extrsimplifymap, erremap, idremap);

				PInfoModel.PIModel sin = summaryin.MakePIModelForThis();
				PInfoModel.PIModel sout = (summaryout != null) ? summaryout.MakePIModelForThis() : null;

				cm.FinalizeSummaryInfo(sin, sout, erremap, idremap);
			}

			//
			Console.WriteLine("Starting Loop Info Pass");

			//process the loop summaries
			foreach(Tuple<IRInvokeIdentity, List<MethodContextState>> mcst in mcstl)
			{
				if(mcst.Item2.Count == 0)
					continue;

				Dictionary<long, AProgramMemory> loopidtobeforeafterbodymap = new Dictionary<long, AProgramMemory>();
				Dictionary<int, int> idsimplifymap = methodidsimplify[mcst.Item1];
				Dictionary<AExternalRef, AExternalRef> extrsimplifymap = methodextrsimplify[mcst.Item1];

				foreach(MethodContextState mmcs in mcst.Item2)
				{
					//gather loop invariants
					foreach(KeyValuePair<long, AProgramMemory> looppmv in mmcs.LoopToEntryInvStateMap)
					{
						AProgramMemory lem = looppmv.Value.CopyMemoryState();
						lem.FinalInfoComputeTidySummary(idsimplifymap, extrsimplifymap);

						if(!loopidtobeforeafterbodymap.ContainsKey(looppmv.Key))
							loopidtobeforeafterbodymap.Add(looppmv.Key, lem);
						else
						{
							lem = AProgramMemory.PMemoryMergeLocalFlow(lem, loopidtobeforeafterbodymap[looppmv.Key], false);
							loopidtobeforeafterbodymap[looppmv.Key] = lem;
						}
					}

					mmcs.LoopToEntryInvStateMap.Clear();
				}

				Dictionary<int, Tuple<PInfoModel.PIModel, PInfoModel.PIModel>> looppim = new Dictionary<int, Tuple<PInfoModel.PIModel, PInfoModel.PIModel>>();
				foreach(KeyValuePair<long, AProgramMemory> loopsumv in loopidtobeforeafterbodymap)
					methodstates[mcst.Item1].LoopIDToBeforeAfterBodyMap.Add(loopsumv.Key, loopsumv.Value.MakePIModelForThis());
			}

			//
			Console.WriteLine("Done Info Completion.");

			return resv;
		}

		private static void DoSetupOfCompleteInfo(Dictionary<IRInvokeIdentity, PInfoModel.CompleteAnalysisInfoMethod> methodstates, Dictionary<IRInvokeIdentity, Dictionary<int, int>> methodidsimplify, Dictionary<IRInvokeIdentity, Dictionary<AExternalRef, AExternalRef>> methodextrsimplify, bool computeprogpointinfo)
		{
			//initialize all the CompleteMethodContexts for computation
			List<Tuple<IRInvokeIdentity, List<MethodContextState>>> mcstl = s_analysis.GetAllMethodsAndContextsForInfoCompletion();
			
			for(int i = 0; i < mcstl.Count; ++i)
			{
				Tuple<IRInvokeIdentity, List<MethodContextState>> mcst = mcstl[i];
				if(mcst.Item2.Count == 0)
					continue;

				List<PInfoModel.CompleteAnalysisInfoMethodContext> iil = new List<PInfoModel.CompleteAnalysisInfoMethodContext>();

				foreach(MethodContextState mmcs in mcst.Item2)
				{
					//set the escape identity information
					Tuple<AProgramMemory, AProgramMemory> resp = mmcs.GetInputOutputPairForCompleteInfo();
					PInfoModel.PIModel min = resp.Item1.MakePIModelForThis();

					//add single context
					PInfoModel.CompleteAnalysisInfoMethodContext cmmc = new PInfoModel.CompleteAnalysisInfoMethodContext(mmcs.ContextID, mmcs.MethodOfCallState, mmcs.CallStateMethodBody, min, mmcs.IsInteralRecursiveCallContext, mmcs.ContextToken, mmcs.EvalPassCount);
					iil.Add(cmmc);
				}

				methodidsimplify.Add(mcst.Item1, new Dictionary<int, int>());
				methodextrsimplify.Add(mcst.Item1, new Dictionary<AExternalRef, AExternalRef>());

				PInfoModel.CompleteAnalysisInfoMethod cm = new PInfoModel.CompleteAnalysisInfoMethod(mcst.Item1, iil, new Dictionary<long, PInfoModel.PIModel>());

				methodstates.Add(mcst.Item1, cm);
			}

			//do the final analysis pass for each method context
			CompleteAnalysisResults = new PInfoModel.CompleteAnalysisInfoForProgram(s_prog, methodstates, computeprogpointinfo);

			int ctrtag = 0;
			ClearOldSerializedData();

			for(int i = 0; i < mcstl.Count; ++i)
			{
				Tuple<IRInvokeIdentity, List<MethodContextState>> mcst = mcstl[i];
				if(mcst.Item2.Count == 0)
					continue;

				foreach(MethodContextState mcs in mcst.Item2)
				{
					GlobalAnalysisState.TAnalysisState.FinalPassSetCurrentMethodEvalState(mcs);
					mcs.CurrentStatus = (mcs.CurrentStatus | ContextStatus.AnalysisInProgress);
					GlobalAnalysisState.CompleteAnalysisResults.CurrentContext = GlobalAnalysisState.CompleteAnalysisResults.LookupInfoForMethodAndContext(mcs.MethodOfCallState, mcs.ContextID);
					GlobalAnalysisState.CompleteAnalysisResults.CurrentProgramPointInfo = new Dictionary<int, PInfoModel.ProgramPointInfo>();

					AProgramMemory pm = mcs.GetCopyOfInputStateForCompute();
					LocalAnalyzer.InfoComplete_AnalyzeBody(mcs.CallStateMethodBody, pm, GlobalAnalysisState.CompleteAnalysisResults.DoProgPointInfoCompute);
					mcs.FinalPassExtractCalleeScopeEscapeToCallerScopeEscapeAndUsedContextUpdate();

					ctrtag++;
					string dumpfile = GetSerializationFilename(ctrtag, mcs.CallStateMethodBody);
					GlobalAnalysisState.CompleteAnalysisResults.CurrentContext.CommitCompleteProgramPointInfo(dumpfile, GlobalAnalysisState.CompleteAnalysisResults.CurrentProgramPointInfo);

					mcs.CurrentStatus = ContextStatus.Clear;
					GlobalAnalysisState.CompleteAnalysisResults.CurrentContext = null;
					GlobalAnalysisState.CompleteAnalysisResults.CurrentProgramPointInfo = null;
					GlobalAnalysisState.TAnalysisState.FinalPassSetCurrentMethodEvalState(null);
				}
			}
		}

		private static void ClearOldSerializedData()
		{
			string[] files = System.IO.Directory.GetFiles(SerializeDataDir, "*.infodmp");
			foreach(string sfn in files)
				System.IO.File.Delete(sfn);
		}

		private static string GetSerializationFilename(int ctr, IRBodyDef bdf)
		{
			string ctn = bdf.InvokeID.DefInClass.BaseTypeName;
			if(ctn.Contains('<'))
			{
				int fl = ctn.IndexOf('<');
				ctn = ctn.Substring(0, fl);
			}

			string bbn = bdf.InvokeID.Sig.InvokeName;
			if(bbn.Contains('.') && !bbn.StartsWith("."))
			{
				int tl = bbn.LastIndexOf('.');
				bbn = bbn.Substring(tl + 1);
			}

			if(bbn.Contains('<'))
				bbn = "NameMangledCompilerDef";

			string mstr = ctn + "@" + bbn + "_" + ctr.ToString() + ".infodmp";
			string fnstr = System.IO.Path.Combine(SerializeDataDir, mstr);
			return fnstr;
		}

		/// <summary>
		/// Get the Program that we are analyzing.
		/// </summary>
		public static IRProgram TProg { get { return s_prog; } }

		/// <summary>
		/// Get the global state of the program analysis.
		/// </summary>
		public static GlobalCallStateMap TAnalysisState { get { return s_analysis; } }

		////////////////////////////////
		//Debugging support messages

		//NOISY, may want to comment the logging out to reduce noise later
		[System.Diagnostics.Conditional("DEBUG_ENABLED")]
		internal static void Display__CallToSig(IRInvokeSig sig)
		{ 
			//Console.WriteLine("    Call to Method with Sig: " + sig.ToString() + "."); 
		}

		[System.Diagnostics.Conditional("DEBUG_ENABLED")]
		internal static void Display__BuiltinExec(IRInvokeIdentity iid)
		{
			//Console.Write("      - Possible Target Of: " + iid.ToString()); 
			//Console.WriteLine(" @ Builtin Exec."); 
		}

		[System.Diagnostics.Conditional("DEBUG_ENABLED")]
		internal static void Display__Memoized(IRInvokeIdentity iid)
		{
			//Console.Write("      - Possible Target Of: " + iid.ToString()); 
			//Console.WriteLine(" @ Memozied."); 
		}

		[System.Diagnostics.Conditional("DEBUG_ENABLED")]
		internal static void Display__MemoizedPartialApproxUsed()
		{
			//Console.WriteLine("            &&Partial Approx. Used."); 
		}
		//NOISY

		[System.Diagnostics.Conditional("DEBUG_ENABLED")]
		internal static void Display__FullyResolvedPendingForCall(IRInvokeIdentity iid)
		{
			Console.Write("      - Possible Target Of: " + iid.ToString()); 
			Console.WriteLine(" @ New Input On Fully Resolved, Freeze and Enqueue.");
		}

		[System.Diagnostics.Conditional("DEBUG_ENABLED")]
		internal static void Display__GeneralPendingForCall(IRInvokeIdentity iid)
		{
			Console.Write("      - Possible Target Of: " + iid.ToString()); 
			Console.WriteLine(" @ New Input On Genreral Call, Freeze and Enqueue."); 
		}

		[System.Diagnostics.Conditional("DEBUG_ENABLED")]
		internal static void Display__GeneralPendingForCallBaseCase(IRInvokeIdentity iid)
		{
			Console.Write("      - Possible Target Of: " + iid.ToString()); 
			Console.WriteLine(" @ Encountered Previous Unprocessed Input State, Freeze and Enqueue."); 
		}

		[System.Diagnostics.Conditional("DEBUG_ENABLED")]
		internal static void Display__PrintPendingInfo()
		{ Console.Write(s_analysis.GetPendingListStrings()); }

		[System.Diagnostics.Conditional("DEBUG_ENABLED")]
		internal static void Display__PrintAnalysisStart(MethodContextState mcs)
		{ Console.WriteLine("\nStarting Analysis on: " + mcs.ToString() + "."); }

		[System.Diagnostics.Conditional("DEBUG_ENABLED")]
		internal static void Display__PrintAnalysisResume(MethodContextState mcs)
		{ Console.WriteLine("\nContinuing Analysis on: " + mcs.ToString() + "."); }

		[System.Diagnostics.Conditional("DEBUG_ENABLED")]
		internal static void Display__PrintAnalysisResultsOutputChanged(bool isfullyresolved)
		{ if(!isfullyresolved) Console.WriteLine("Output Changed."); }

		[System.Diagnostics.Conditional("DEBUG_ENABLED")]
		internal static void Display__PrintAnalysisResultsOutputStable(bool isfullyresolved)
		{ if(!isfullyresolved) Console.WriteLine("Output Stable."); }

		[System.Diagnostics.Conditional("DEBUG_ENABLED")]
		internal static void Display__PrintAnalysisResultsInputChanged()
		{ Console.WriteLine("Input Changed."); }

		[System.Diagnostics.Conditional("DEBUG_ENABLED")]
		internal static void Display__PrintAnalysisResultsFreezing()
		{ Console.WriteLine("    Freezing."); }

		[System.Diagnostics.Conditional("DEBUG_ENABLED")]
		internal static void Display__PrintAnalysisAnalysisComplete()
		{ Console.WriteLine("Analysis Complete."); }
	}

	////////////////////////////////////////////////////////////////////
	////////////////////////////////////////////////////////////////////
	/// <summary>
	/// Track the memoized input/output relations for path specific calls to fully resolved components and the current approximations for 
	/// all other calls calls. We are going to have one of these as a static value for the whole program.
	/// </summary>
	public sealed class GlobalCallStateMap
	{
		/// <summary>
		/// When there are 10 or more null weak refs in a context list we will clear them.
		/// </summary>
		private const int NULL_CLEAR_THRESHOLD = 10;

		/// <summary>
		/// For methods that are fully resolved this maps to the call context and then the specific call contexts.
		/// The int is the bound for our next elim operation.
		/// </summary>
		private readonly Dictionary<IRBodyDef, List<WeakReference>> m_contextsMemoMap;

		/// <summary>
		/// A worklist of approximate method eval contexts that we want to process.
		/// </summary>
		private readonly LinkedList<MethodContextState> m_pendingGeneralFixpointContextsWorklist;

		/// <summary>
		/// A random number generator to pick one of the pending methods in a scc to process.
		/// </summary>
		private readonly Random m_sccrandchoice;

		/// <summary>
		/// A List (which we access in a stack like fashion) that has the call stack for evaluating fully resolved call chains.
		/// </summary>
		private readonly LinkedList<MethodContextState> m_pendingFullyResolvedStack;

		/// <summary>
		/// The method eval state that is currently being analyzed.
		/// </summary>
		private MethodContextState m_currentMethodEvalState;

		/// <summary>
		/// For generating fresh method context ids.
		/// </summary>
		private int m_methodcontextidctr;

		/// <summary>
		/// If a breakpoint is set this is the line number that it is on.
		/// </summary>
		private int m_stmtBrkID;

		[ContractInvariantMethod]
		private void ObjectInvariant()
		{
			Contract.Invariant(this.m_contextsMemoMap != null);
			Contract.Invariant(this.m_pendingGeneralFixpointContextsWorklist != null);
			Contract.Invariant(this.m_pendingFullyResolvedStack != null);
			Contract.Invariant(this.m_sccrandchoice != null);

			Contract.Invariant(this.m_currentMethodEvalState != null || this.m_pendingGeneralFixpointContextsWorklist.Count == 0);
		}

		internal GlobalCallStateMap()
		{
			this.m_contextsMemoMap = new Dictionary<IRBodyDef, List<WeakReference>>();
			this.m_pendingGeneralFixpointContextsWorklist = new LinkedList<MethodContextState>();
			this.m_sccrandchoice = new Random(1);

			this.m_pendingFullyResolvedStack = new LinkedList<MethodContextState>();

			this.m_currentMethodEvalState = null;

			this.m_methodcontextidctr = 1;

#if DEBUG_ENABLED
			this.m_stmtBrkID = 0;
#else
			this.m_stmtBrkID = 10000000;
#endif
		}

		internal void InitializeForAnalysis(CallGraph cg, BodyDefTable bdt)
		{
			foreach(CallGraphNode cgn in cg.Nodes)
				this.m_contextsMemoMap.Add(bdt.GetBodyForInvokeExactSigMatch(cgn.Def), new List<WeakReference>());
		}

		/// <summary>
		/// Gather statistics for overall analysis costs and times.
		/// </summary>
		public void ComputeAverageMemoContextInfo(out double averageCTX, out double averageprocs, out int maxCTX, out int maxprocs, out int maxnodes, out int maxedges)
		{
			double tct = 0.0;
			int ct = 0;

			double tvc = 0.0;
			int cct = 0;

			maxCTX = 0;
			maxprocs = 0;

			maxnodes = 0;
			maxedges = 0;

			foreach(KeyValuePair<IRBodyDef, List<WeakReference>> smm in this.m_contextsMemoMap)
			{
				if(smm.Value.Count != 0)
				{
					tct += smm.Value.Count((WeakReference wr) => wr.IsAlive);
					ct++;
				}

				if(smm.Value.Count > maxCTX)
					maxCTX = smm.Value.Count;

				foreach(WeakReference wcss in smm.Value)
				{
					MethodContextState mcss = (MethodContextState)wcss.Target;
					if(mcss == null)
						continue;

					tvc += mcss.EvalPassCount;
					cct++;

					if(mcss.EvalPassCount > maxprocs)
						maxprocs = mcss.EvalPassCount;

					int nodecount = mcss.GetInputContextForCompare().Memory.Count((ALocation ll) => ll is AObject);
					maxnodes = Math.Max(maxnodes, nodecount);

					int edgecount = mcss.GetInputContextForCompare().Memory.Where((ALocation ll) => ll is AObject).Aggregate(0, (int accum, ALocation ll) => accum + ((AObject)ll).StructOrClassPointers.PTargetCount);
					maxedges = Math.Max(edgecount, maxedges);
				}
			}

			averageCTX = tct / ct;
			averageprocs = tvc / cct;
		}

		/// <summary>
		/// Eliminate all the call contexts that do not have ids in the given set.
		/// </summary>
		internal void ForceCleanUselessContexts(MethodContextState mainctx, HashSet<int> okctxids)
		{
			Queue<MethodContextState> pending = new Queue<MethodContextState>();
			pending.Enqueue(mainctx);

			while(pending.Count != 0)
			{
				MethodContextState ntctx = pending.Dequeue();
				okctxids.Add(ntctx.ContextID);

				foreach(MethodContextState depon in ntctx.ContextIDsUsedLastPass)
				{
					if(!okctxids.Contains(depon.ContextID))
						pending.Enqueue(depon);
				}
			}

			foreach(KeyValuePair<IRBodyDef, List<WeakReference>> kkvp in this.m_contextsMemoMap)
			{
				for(int i = 0; i < kkvp.Value.Count; ++i)
				{
					WeakReference wr = kkvp.Value[i];
					MethodContextState mmcs = (MethodContextState)wr.Target;
					if(mmcs != null && !okctxids.Contains(mmcs.ContextID))
						wr.Target = null;
				}

				kkvp.Value.RemoveAll((WeakReference wr) => wr.Target == null);
			}
		}

		/// <summary>
		/// Return a list of the identities and all contexts for every method that is analyzed in the program. This is used 
		/// to construct the full program info which is used in later analysis.
		/// </summary>
		internal List<Tuple<IRInvokeIdentity, List<MethodContextState>>> GetAllMethodsAndContextsForInfoCompletion()
		{
			List<Tuple<IRInvokeIdentity, List<MethodContextState>>> rl = new List<Tuple<IRInvokeIdentity, List<MethodContextState>>>();
			foreach(KeyValuePair<IRBodyDef, List<WeakReference>> kkvp in this.m_contextsMemoMap)
			{
				List<MethodContextState> mcls = new List<MethodContextState>();
				foreach(WeakReference wr in kkvp.Value)
				{
					MethodContextState mmcs = (MethodContextState)wr.Target;
					Contract.Assert(mmcs != null, "We should clear all unused contexts before calling this!!!");

					mcls.Add(mmcs);
				}

				rl.Add(new Tuple<IRInvokeIdentity, List<MethodContextState>>(kkvp.Key.InvokeID, mcls));
			}

			return rl;
		}

		/// <summary>
		/// Return an string with some extra information if there are models associated with this, null if this call is never reached.
		/// </summary>
		public List<Tuple<AProgramMemory, AProgramMemory, AProgramMemory>> GetDisplayAndAnalysisPairsForBody(IRBodyDef b, out int totalvisits)
		{
			Contract.Requires(b != null);
			Contract.Ensures(Contract.Result<List<Tuple<AProgramMemory, AProgramMemory>>>() != null);

			totalvisits = 0;
			List<Tuple<AProgramMemory, AProgramMemory, AProgramMemory>> resl = new List<Tuple<AProgramMemory, AProgramMemory, AProgramMemory>>();
			if(this.m_contextsMemoMap.ContainsKey(b))
			{
				List<WeakReference> csmel = this.m_contextsMemoMap[b];
				for(int i = 0; i < csmel.Count; ++i)
				{
					MethodContextState mcs = (MethodContextState)csmel[i].Target;
					if(mcs == null)
						continue;

					totalvisits += mcs.EvalPassCount;
					mcs.LoadPairForDisplayOrAnalysis(resl);
				}
			}

			return resl;
		}

		///////////////////////////////////
		//Lookup memoized states

		/// <summary>
		/// Return thematching memoized state for a fully resolved call or instatiate a new one if needed, return the context state (and the <c>MatchCase</c> 
		/// to indicate how the call was resolved), update the maps <c>idremap</c> and <c>extrefmap</c> with the mapping info if it is not a fresh match.
		/// If a new context is created this takes possesion of <c>callpm</c> (e.g., whenever the return value Item1 is <c>FreshMatch</c>).
		/// </summary>
		internal MethodContextState HasMemoForCallAddMemoContextAsNeeded(IRBodyDef b, AProgramMemory callpm, bool isrecursive, IRType contexttoken, CallStateSubMap csm)
		{
			Contract.Requires(b != null);
			Contract.Requires(callpm != null && (!callpm.IsInfeasable));
			Contract.Requires(csm != null);
			Contract.Ensures(Contract.Result<MethodContextState>() != null);

			int nullcount = 0;
			List<WeakReference> mev = this.m_contextsMemoMap[b];

			//check for domain equality match
			if(!isrecursive)
			{
				for(int i = 0; i < mev.Count; ++i)
				{
					MethodContextState mcs = (MethodContextState)mev[i].Target;
					if(mcs == null)
					{
						nullcount++;
						continue;
					}

					if((!mcs.IsInteralRecursiveCallContext) & (mcs.ContextToken == contexttoken))
					{
						AProgramMemory inputstate = mcs.GetInputContextForCompare();
						if(AProgramMemory.EquivOnCallEntry(inputstate, callpm, csm))
						{
							if(nullcount >= NULL_CLEAR_THRESHOLD)
								mev.RemoveAll((WeakReference wr) => wr.Target == null);

							//note that the equiv check will have filled csm with the correct values
							return mcs;
						}
					}
				}
 			}
			else
			{
				for(int i = 0; i < mev.Count; ++i)
				{
					MethodContextState mcs = (MethodContextState)mev[i].Target;
					if(mcs == null)
					{
						nullcount++;
						continue;
					}

					if(mcs.IsInteralRecursiveCallContext & (mcs.ContextToken == contexttoken))
					{
						Contract.Assert(!mcs.CallStateMethodBody.InvokeID.Sig.InvokeSig.Any((IRType tt) => tt is IRReferenceType), "We would need to be more careful of this.");

						//note that the equiv check will fill in csm with the correct values
						AProgramMemory inputstate = mcs.GetInputContextForCompare();
						AMemEqPartition pmcs = AProgramMemory.PMemoryMergeCallsPartition(inputstate, callpm);
						inputstate.BuildCallStateMapForSubsume_OptionalCheckSubsume(callpm, pmcs, csm, true);
						if(csm.OutCase == MatchCase.SubsumeAlter)
							mcs.UpdateInApproxOnNotSubsumed(callpm);

						return mcs;
					}
				}
			}

			if(nullcount >= NULL_CLEAR_THRESHOLD)
				mev.RemoveAll((WeakReference wr) => wr.Target == null);

			MethodContextState nmcs = new MethodContextState(b.InvokeID, b, callpm, this.m_methodcontextidctr++, isrecursive, contexttoken);
			mev.Add(new WeakReference(nmcs));
			csm.OutCase = MatchCase.FreshMatch;
			return nmcs;
		}

		///////////////////////////////////
		//Manage the worklists

		internal String GetPendingListStrings()
		{
			bool first;
			StringBuilder sb = new StringBuilder();

			first = true;
			sb.Append("ResolvedPendingStack:\n[\n");
			foreach(MethodContextState mcsn in this.m_pendingFullyResolvedStack)
			{
				if(!first)
					sb.Append(", \n");
				first = false;
				sb.Append("  " + mcsn.ToString());
			}
			sb.Append("\n]\n\n");

			first = true;
			sb.Append("GeneralPendingList:\n[\n");
			foreach(MethodContextState mcsn in this.m_pendingGeneralFixpointContextsWorklist)
			{
				if(!first)
					sb.Append(", \n");
				first = false;
				sb.Append("  " + mcsn.ToString());
			}
			sb.Append("\n]\n");

			return sb.ToString();
		}

		/// <summary>
		/// Process the next method in order.
		/// </summary>
		internal bool ProcessNextPendingMethod(CallGraph cg)
		{
			//get the next method to process
			MethodContextState cmcs = this.GetNextPendingMethod(cg);

			if((cmcs.CurrentStatus & ContextStatus.AnalysisInProgress) == ContextStatus.Clear)
				cmcs.EvalPassCount++;

			this.m_currentMethodEvalState = cmcs;
			CallGraphNode cgn = cg.GetCallNodeForInvokeIdentity(cmcs.MethodOfCallState);
			LocalAnalysisResult resv;

			if(cmcs.IsNewInputPending || (cmcs.CurrentStatus & ContextStatus.AnalysisInProgress) == ContextStatus.Clear)
			{
				GlobalAnalysisState.Display__PrintAnalysisStart(cmcs);

				cmcs.CurrentStatus = (cmcs.CurrentStatus | ContextStatus.AnalysisInProgress);
				AProgramMemory m = cmcs.GetCopyOfInputStateForCompute();
				resv = LocalAnalyzer.AnalyzeBodyStart(cmcs.CallStateMethodBody, m);
			}
			else
			{
				GlobalAnalysisState.Display__PrintAnalysisResume(cmcs);

				resv = LocalAnalyzer.AnalyzeBodyResume();
			}

			if(resv == LocalAnalysisResult.FrozenForCall)
			{
				GlobalAnalysisState.Display__PrintAnalysisResultsFreezing();

				LinkedListNode<MethodContextState> mcsl;
				if(cg.IsCallFullySimple_StaticCallGraph(cgn.Def))
					mcsl = this.m_pendingFullyResolvedStack.Find(null);
				else
					mcsl = this.m_pendingGeneralFixpointContextsWorklist.Find(null);
				
				mcsl.Value = cmcs;
			}
			else
			{
				bool resultchanged = cmcs.UpdateReturnContextNoteIfChanged();

				if(cmcs.IsNewInputPending | resultchanged)
				{
					GlobalAnalysisState.Display__PrintAnalysisResultsOutputChanged(cg.IsCallFullySimple_StaticCallGraph(cgn.Def));
					this.OutputOfMethodChangedMarkNeeded(cmcs, cg);
				}
				else
					GlobalAnalysisState.Display__PrintAnalysisResultsOutputStable(cg.IsCallFullySimple_StaticCallGraph(cgn.Def));

				if(cg.IsCallFullySimple_StaticCallGraph(cgn.Def))
					this.m_pendingFullyResolvedStack.Remove((MethodContextState)null);
				else
				{
					cmcs.CurrentStatus &= ~(ContextStatus.OnPendingList);
					this.m_pendingGeneralFixpointContextsWorklist.Remove((MethodContextState)null);
				}
				

				//if it has a child output dependency then re-insert in it in the list
				if(cmcs.IsNewInputPending | ((cmcs.CurrentStatus & (ContextStatus.DependsOnOutputUpdated)) != ContextStatus.Clear))
				{
					cmcs.CurrentStatus = (cmcs.CurrentStatus & ~(ContextStatus.DependsOnOutputUpdated | ContextStatus.AnalysisInProgress));
					this.EnqueueIntoGeneralListInRightLocation(cmcs, cg);
				}
				else
				{
					GlobalAnalysisState.Display__PrintAnalysisAnalysisComplete();

					cmcs.CurrentStatus = ContextStatus.Clear;
				}
			}

			////
			Contract.Assert(((cmcs.CurrentStatus & ContextStatus.OnPendingList) == ContextStatus.OnPendingList) == (this.m_pendingFullyResolvedStack.Contains(cmcs) || this.m_pendingGeneralFixpointContextsWorklist.Contains(cmcs)), "Marked a on lists but it isn't there.");
			
			//return true if we are done
			this.m_currentMethodEvalState = null;
			return (this.m_pendingFullyResolvedStack.Count == 0) & (this.m_pendingGeneralFixpointContextsWorklist.Count == 0);
		}

		private int CompareWorklistEntries(MethodContextState mcs1, MethodContextState mcs2, CallGraph cg)
		{
			CallGraphNode cgn1 = cg.GetCallNodeForInvokeIdentity(mcs1 == null ? this.m_currentMethodEvalState.MethodOfCallState : mcs1.MethodOfCallState);
			CallGraphNode cgn2 = cg.GetCallNodeForInvokeIdentity(mcs2 == null ? this.m_currentMethodEvalState.MethodOfCallState : mcs2.MethodOfCallState);

			return cgn1.DFSFinishTime - cgn2.DFSFinishTime;
		}

		/// <summary>
		/// Get next method to process.
		/// </summary>
		internal MethodContextState GetNextPendingMethod(CallGraph cg)
		{
			Contract.Assert((new HashSet<MethodContextState>(this.m_pendingFullyResolvedStack)).Count ==  this.m_pendingFullyResolvedStack.Count);
			Contract.Assert((new HashSet<MethodContextState>(this.m_pendingGeneralFixpointContextsWorklist)).Count == this.m_pendingGeneralFixpointContextsWorklist.Count);
			Contract.Assert(Contract.ForAll(this.m_pendingGeneralFixpointContextsWorklist, (MethodContextState mcs) => (mcs.CurrentStatus & ContextStatus.OnPendingList) != ContextStatus.Clear));

			LinkedListNode<MethodContextState> wlnode;
			MethodContextState wlnext;

			if(this.m_pendingFullyResolvedStack.Count != 0)
			{
				wlnext = this.m_pendingFullyResolvedStack.Last.Value;
				this.m_pendingFullyResolvedStack.Last.Value = null;
			}
			else
			{
				if(cg.UpdatedGraph)
				{
					cg.UpdatedGraph = false;
					cg.RecomputeDFS();

					MethodContextState[] ssa = new MethodContextState[this.m_pendingGeneralFixpointContextsWorklist.Count];
					this.m_pendingGeneralFixpointContextsWorklist.CopyTo(ssa, 0);
					this.m_pendingGeneralFixpointContextsWorklist.Clear();

					Array.Sort(ssa, (MethodContextState mcs1, MethodContextState mcs2) => this.CompareWorklistEntries(mcs1, mcs2, cg));
					for(int i = 0; i < ssa.Length; ++i)
						this.m_pendingGeneralFixpointContextsWorklist.AddLast(ssa[i]);
				}

				wlnode = this.m_pendingGeneralFixpointContextsWorklist.First;
				IRInvokeIdentity iiv = wlnode.Value.MethodOfCallState;
				if(cg.IsCallInSCC_StaticCallGraph(iiv))
				{
					List<LinkedListNode<MethodContextState>> sccmembers = new List<LinkedListNode<MethodContextState>>();
					while(wlnode != null)
					{
						if(cg.AreCallsInSameSCC_StaticCallGraph(iiv, wlnode.Value.MethodOfCallState))
							sccmembers.Add(wlnode);

						wlnode = wlnode.Next;
					}

					//if there are entries which have never been processed then run them before re-running other states
					if(sccmembers.Exists((LinkedListNode<MethodContextState> mcsle) => mcsle.Value.EvalPassCount == 0))
						sccmembers.RemoveAll((LinkedListNode<MethodContextState> mcsle) => mcsle.Value.EvalPassCount != 0);

					Comparison<LinkedListNode<MethodContextState>> ff = ((LinkedListNode<MethodContextState> mcss1, LinkedListNode<MethodContextState> mcss2) => this.CompareWorklistEntries(mcss1.Value, mcss2.Value, cg));
					sccmembers.Sort(ff);
					int randloc = this.m_sccrandchoice.Next(sccmembers.Count);
					wlnode = sccmembers[randloc];
					
					wlnext = wlnode.Value;
					wlnode.Value = null;
				}
				else
				{
					MethodContextState pfcs = wlnode.Value;
					List<LinkedListNode<MethodContextState>> samescores = new List<LinkedListNode<MethodContextState>>();
					while(wlnode != null && this.CompareWorklistEntries(pfcs, wlnode.Value, cg) == 0)
					{
						samescores.Add(wlnode);
						wlnode = wlnode.Next;
					}

					Comparison<LinkedListNode<MethodContextState>> ff = ((LinkedListNode<MethodContextState> mcss1, LinkedListNode<MethodContextState> mcss2) => this.CompareWorklistEntries(mcss1.Value, mcss2.Value, cg));
					samescores.Sort(ff);
					int randloc = this.m_sccrandchoice.Next(samescores.Count);
					wlnode = samescores[randloc];

					wlnext = wlnode.Value;
					wlnode.Value = null;
				}
			}

			return wlnext;
		}

		/// <summary>
		/// When we have method context that needs to be processed do to a call to it use this to enqueue it for processing relative to the current context.
		/// </summary>
		internal void EnqueueCalleeMethod(MethodContextState mcs, CallGraph cg)
		{
			Contract.Requires(mcs != null);
			Contract.Requires(cg != null);

			if(mcs != this.m_currentMethodEvalState)
			{
				DebugState ndbgstate = (this.m_currentMethodEvalState != null ? this.m_currentMethodEvalState.DebugState : mcs.DebugState);
				mcs.DebugState = (ndbgstate == DebugState.DebugStepInto) ? DebugState.DebugStep : ((DebugState)Math.Min((int)DebugState.DebugBreakAt, (int)ndbgstate)); //step into -> step, run->run other stays as is
			}

			CallGraphNode mcgn = cg.GetCallNodeForInvokeIdentity(mcs.MethodOfCallState);
			if(cg.IsCallFullySimple_StaticCallGraph(mcgn.Def))
			{
				mcs.CurrentStatus = (mcs.CurrentStatus | ContextStatus.OnPendingList);
				this.m_pendingFullyResolvedStack.AddLast(mcs);
			}
			else
			{
				this.EnqueueIntoGeneralListInRightLocation(mcs, cg);
			}
		}

		/// <summary>
		/// Take a method context state that needs to be enqued in the worklist and put it in the correct position
		/// </summary>
		private void EnqueueIntoGeneralListInRightLocation(MethodContextState mcs, CallGraph cg)
		{
			Contract.Requires(mcs != null);
			Contract.Requires(cg != null);

			CallGraphNode mcgn = cg.GetCallNodeForInvokeIdentity(mcs.MethodOfCallState);
			Contract.Assert(!cg.IsCallFullySimple_StaticCallGraph(mcgn.Def));

			if((mcs.CurrentStatus & ContextStatus.OnPendingList) == ContextStatus.Clear)
			{
				//if this context is not on the pending list then add it
				mcs.CurrentStatus = (mcs.CurrentStatus | ContextStatus.OnPendingList);

				LinkedListNode<MethodContextState> wlpos = this.m_pendingGeneralFixpointContextsWorklist.First;
				while(wlpos != null)
				{
					if(this.CompareWorklistEntries(wlpos.Value, mcs, cg) >= 0)
						break;

					wlpos = wlpos.Next;
				}

				if(wlpos == null)
					this.m_pendingGeneralFixpointContextsWorklist.AddLast(mcs);
				else
					this.m_pendingGeneralFixpointContextsWorklist.AddBefore(wlpos, mcs);
			}
		} 

		/// <summary>
		/// When we have finished analyzing a method use this to add any contexts that depend on it.
		/// </summary>
		internal void OutputOfMethodChangedMarkNeeded(MethodContextState mcs, CallGraph cg)
		{
			Contract.Requires(mcs != null);
			Contract.Requires(cg != null);

			CallGraphNode mcgn = cg.GetCallNodeForInvokeIdentity(mcs.MethodOfCallState);
			if(cg.IsCallFullySimple_StaticCallGraph(mcgn.Def))
			{
				//Things are easy because we always do full call graph cloning and stack order when we are doing 
				//fully simple calls. So if we are the caller must already be pending so we don't need to do anything.
			}
			else
			{
				List<MethodContextState> deponctxts = new List<MethodContextState>();

				for(int i = 0; i < mcgn.CallInList.Count; ++i)
				{
					CallGraphEdge cge = mcgn.CallInList[i];
					CallGraphNode ccgn = cg.GetCallNodeForInvokeIdentity(cge.CallerIdentity);
					IRBodyDef assocbody = GlobalAnalysisState.TProg.MethodBodyTable.GetBodyForInvokeExactSigMatch(ccgn.Def);
					List<WeakReference> pdepmcls = this.m_contextsMemoMap[assocbody];

					for(int j = 0; j < pdepmcls.Count; ++j)
					{
						MethodContextState pdep = (MethodContextState)pdepmcls[j].Target;
						if(pdep == null)
							continue;

						if(pdep.ContextIDsUsedCurrentPass.Contains(mcs) || pdep.ContextIDsUsedLastPass.Contains(mcs))
							deponctxts.Add(pdep);
					}
				}

				for(int i = 0; i < deponctxts.Count; ++i)
				{
					MethodContextState mctx = deponctxts[i];
					mctx.CurrentStatus = (mctx.CurrentStatus | ContextStatus.DependsOnOutputUpdated);
					this.EnqueueIntoGeneralListInRightLocation(mctx, cg);
				}
			}
		}

		/// <summary>
		/// At the end of the analysis clear all the context states that we generated as intermediate states 
		/// but no longer need.
		/// </summary>
		internal void ClearUnUsedStates()
		{
			//run a full GC to clear out any dead method contexts that are only around because of weak references.
			System.GC.Collect();
			foreach(List<WeakReference> mcsl in this.m_contextsMemoMap.Values)
				mcsl.RemoveAll((WeakReference wr) => !wr.IsAlive);
		}

		/// <summary>
		/// The method eval state that is currently being analyzed.
		/// </summary>
		internal void FinalPassSetCurrentMethodEvalState(MethodContextState fmcs)
		{ this.m_currentMethodEvalState = fmcs; }

		///////////////////////////////////
		//Accessors

		/// <summary>
		/// The method eval state that is currently being analyzed.
		/// </summary>
		internal MethodContextState CurrentMethodEvalState
		{
			get
			{
				Contract.Ensures(Contract.Result<MethodContextState>() != null);

				return this.m_currentMethodEvalState;
			}
		}

		/// <summary>
		/// Get/Set the statement number for a breakpoint.
		/// </summary>
		internal int BreakStatementID
		{
			get { return this.m_stmtBrkID; }
			set { this.m_stmtBrkID = value; }
		}
	}
}

